﻿using System;
using System.Diagnostics.Contracts;
using System.IO;

namespace O1.IO
{
    [ContractVerification(true)]
    public abstract class InputAdapter : IDisposable
    {
        private readonly byte[] rawBuffer;

        private int max;

        protected InputAdapter()
        {
            Contract.Ensures(this.rawBuffer != null);
            this.rawBuffer = BufferCache8K.Acquire();
        }

        public int CurrentOffset { get; private set; }

        public bool EndOfStream
        {
            get
            {
                return this.max < 0;
            }
        }

        internal byte[] SharedBuffer
        {
            get
            {
                return this.rawBuffer;
            }
        }

        protected abstract long UnderlyingPosition { get; }

        protected abstract long UnderlyingSize { get; }

        public void Dispose()
        {
            this.Dispose(true);
            GC.SuppressFinalize(this);
        }

        internal bool TryPopOffset(int nextSize, out int offset)
        {
            Contract.Requires(0 <= nextSize);
            Contract.Ensures(this.SharedBuffer.Length == BufferCache8K.Size);
            Contract.Ensures(
                !Contract.Result<bool>() || 
                (Contract.Result<bool>() && (Contract.ValueAtReturn<int>(out offset) + nextSize < this.SharedBuffer.Length)) ||
                this.EndOfStream);

            var nextOffset = this.CurrentOffset + nextSize;
            if (nextOffset >= this.max)
            {
                Contract.Assume(this.max >= this.CurrentOffset);
                
                int bytesRead;
                if (this.TryShiftBuffer(nextSize, out bytesRead))
                {
                    if (bytesRead == 0)
                    {
                        this.max = -1;
                        offset = -1;
                        return true;
                    }
                }
                else
                {
                    offset = 0;
                    return false;
                }

                Contract.Assume(bytesRead < this.rawBuffer.Length);
                Contract.Assume(0 < bytesRead);
                this.max = bytesRead;
                this.CurrentOffset = Math.Min(nextSize, bytesRead);
                offset = 0;

                Contract.Assume(offset + nextSize < this.SharedBuffer.Length);
                return true;
            }

            offset = this.CurrentOffset;
            this.CurrentOffset = nextOffset;
            return true;
        }

        internal int PopOffset(int nextSize)
        {
            Contract.Requires(0 <= nextSize);
            Contract.Requires(BufferCache8K.Size > nextSize);
            Contract.Ensures(-1 <= Contract.Result<int>());
            Contract.Ensures(Contract.Result<int>() < this.rawBuffer.Length);
            Contract.Ensures(this.SharedBuffer.Length == BufferCache8K.Size);
            Contract.Ensures(Contract.Result<int>() + nextSize < this.SharedBuffer.Length);

            if (this.max == -1)
            {
                return -1;
            }

            var nextOffset = this.CurrentOffset + nextSize;
            if (nextOffset >= this.max)
            {
                Contract.Assume(this.max >= this.CurrentOffset);

                int bytesRead;
                if (this.TryShiftBuffer(nextSize, out bytesRead))
                {
                    if (bytesRead == 0)
                    {
                        this.max = -1;
                        return -1;
                    }

                    Contract.Assume(bytesRead < this.rawBuffer.Length);
                    Contract.Assume(bytesRead >= nextSize);

                    this.max = bytesRead;
                    this.CurrentOffset = nextSize;
                    return 0;
                }
                else
                {
                    throw new InvalidOperationException(ExceptionText.SizeExceeds8KBuffer.ToFormat(nextSize));
                }
            }

            var lastOffset = this.CurrentOffset;
            this.CurrentOffset = nextOffset;
            return lastOffset;
        }

        internal int PeekAhead(int offset)
        {
            Contract.Requires(0 <= offset);

            var peekIndex = this.CurrentOffset + offset;
            if (peekIndex >= this.UnderlyingSize)
            {
                return -1;
            }

            if (peekIndex < this.max)
            {
                return this.SharedBuffer[this.CurrentOffset + offset];
            }

            var currentPosition = this.UnderlyingPosition;
            var underlyingOffset = peekIndex - currentPosition;
            this.Seek(underlyingOffset, SeekOrigin.Current);
            var value = this.Read();

            Contract.Assume(underlyingOffset > long.MinValue);
            this.Seek(0 - underlyingOffset, SeekOrigin.Current);
            return value;
        }

        protected abstract int ReadToBuffer(byte[] buffer, int offset, int count);

        protected abstract int Read();

        protected abstract void Seek(long offset, SeekOrigin origin);

        protected virtual void Dispose(bool disposing)
        {
            if (disposing)
            {
                Contract.Assert(this.rawBuffer.Length >= BufferCache8K.Size);
                BufferCache8K.Release(this.rawBuffer);
            }
        }

        private bool TryShiftBuffer(int nextSize, out int bytesRead)
        {
            Contract.Requires(this.max >= this.CurrentOffset);
            Contract.Ensures(
               !Contract.Result<bool>() ||
               (Contract.Result<bool>() && (this.max - this.CurrentOffset + nextSize < this.SharedBuffer.Length)));

            var buffer = this.rawBuffer;
            var remainder = this.max - this.CurrentOffset;
            if (remainder + nextSize >= BufferCache8K.Size)
            {
                bytesRead = 0;
                return false;
            }

            Contract.Assert(this.max - this.CurrentOffset + nextSize < this.SharedBuffer.Length);
            Contract.Assert(remainder > -1);
            Contract.Assert(this.max < buffer.Length);
            Contract.Assert(this.CurrentOffset + remainder < buffer.Length);
            if (remainder > 0)
            {
                Array.Copy(buffer, this.CurrentOffset, buffer, 0, remainder);
            }

            bytesRead = this.ReadToBuffer(buffer, remainder, BufferCache8K.Size - remainder) + remainder;
            Contract.Assume(this.max - this.CurrentOffset + nextSize < this.SharedBuffer.Length);
            return true;
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(this.rawBuffer.Length == BufferCache8K.Size);
            Contract.Invariant(this.max < this.rawBuffer.Length);
            Contract.Invariant(this.max == -1 || this.max >= this.CurrentOffset);
            Contract.Invariant(0 <= this.CurrentOffset);
        }
    }
}
